star-append(T; P; Q)(L)
== LL:T List List
== L':T List. (l_all(LL; (T List); X.(P(X)))  (Q(L'))  (L = append(concat(LL); L'))) 

latex

---

clarification:

star-append(T; P; Q)(L)
== LL:T List List
== L':T List
== (l_all(LL; (T List); X.(P(X)))  (Q(L'))  (L = append(concat(LL); L')  (T List))) 

latex

Definitions	star-append(T; P; Q), x:A. B(x), l_all(L; T; x.P(x)), P  Q, append(as; bs), concat(ll)
FDL editor aliases	star-append